(set-logic QF_LIA)
(set-info :status unsat)
(declare-const Cells_0_0 Int)
(assert (>= Cells_0_0 0))
(declare-const Columns_0_0 Int)
(assert (>= Columns_0_0 0))
(declare-const Regions_0_0 Int)
(assert (>= Regions_0_0 0))
(declare-const Rows_0_0 Int)
(assert (>= Rows_0_0 0))
(declare-const Board_0_0_0 Int)
(assert (>= Board_0_0_0 0))
(declare-const a1 Int)
(assert (>= a1 0))
(assert (= Columns_0_0 Cells_0_0))
(assert (= Regions_0_0 Cells_0_0))
(assert (= Rows_0_0 Cells_0_0))
(assert (= a1 (+ Board_0_0_0 Cells_0_0)))
(assert (= a1 1))
(assert (not (or (not (or (or (and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))(and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1)))(and (and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))(and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1)))))(or (and (and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))(or (and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))(and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))))(not (and (and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))(and (>= Cells_0_0 1)(>= Columns_0_0 1)(>= Regions_0_0 1)(>= Rows_0_0 1))))))))
(check-sat)
(exit)
